package sketchguided.sat4j;

import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStream;
import java.io.PrintWriter;

import org.sat4j.BasicLauncher;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Pair;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.learning.ActiveLearning;
import org.sat4j.minisat.restarts.ArminRestarts;
import org.sat4j.minisat.uip.DecisionUIP;
import org.sat4j.reader.DimacsReader;
import org.sat4j.reader.InstanceReader;
import org.sat4j.reader.LecteurDimacs;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.tools.DecisionTracing;

import sketch.ounit.Values;

import junit.framework.Test;
import junit.framework.TestCase;
import junit.framework.TestSuite;

public class SAT4JConstrainTest extends TestCase {
	
	public static Test suite() {
		return new TestSuite(SAT4JConstrainTest.class);
	}
	
//	public void testLaunchSAT4J() {
//		String[] args = new String[]{"./subjects/sketchguided/sat4j/sample.cnf"};
//		BasicLauncher<ISolver> lanceur = new BasicLauncher<ISolver>(
//				SolverFactory.instance());
//		if (args.length != 1) {
//			lanceur.usage();
//			return;
//		}
//		lanceur.run(args);
//	}
	
//	public void testSAT4JSolver() throws Exception {
//		String problemName = "./subjects/sketchguided/sat4j/sample.cnf";
//		
//		ISolver asolver = SolverFactory.instance().defaultSolver();
//		asolver.setTimeout(Integer.MAX_VALUE);
//		asolver.setDBSimplificationAllowed(true);
//		
//		Solver solver = (Solver)asolver;
//		
//		Values.randomFuzz(solver, Solver.class, VecInt.class, Vec.class, WLClause.class,
//				Pair.class, SearchParams.class, ArminRestarts.class, ActiveLearning.class
//				, DecisionTracing.class, DecisionUIP.class);
//	}
	
//	public void testSAT4JProblem() throws Exception {
//        String problemName = "./subjects/sketchguided/sat4j/sample.cnf";
//		
//		ISolver asolver = SolverFactory.instance().defaultSolver();
//		asolver.setTimeout(Integer.MAX_VALUE);
//		asolver.setDBSimplificationAllowed(true);
//		
//		Reader reader = new InstanceReader(asolver);
//		IProblem problem = reader.parseInstance(problemName);
//	System.out.println("The problem is: " + problem.getClass());
////	
////	Values.randomFuzz((Solver)problem, Solver.class, VecInt.class, Vec.class, WLClause.class,
////			Pair.class, SearchParams.class, ArminRestarts.class, ActiveLearning.class
////			, DecisionTracing.class, DecisionUIP.class);
//	}
	
//	public void testSAT4JReader() throws Exception {
//       String problemName = "./subjects/sketchguided/sat4j/sample.cnf";
//		
//		ISolver asolver = SolverFactory.instance().defaultSolver();
//		asolver.setTimeout(Integer.MAX_VALUE);
//		asolver.setDBSimplificationAllowed(true);
//		
//		DimacsReader reader = new DimacsReader(asolver);
//		Values.randomFuzz(reader, DimacsReader.class, InputStream.class, PrintWriter.class);
//		
//		LecteurDimacs dimacs = new LecteurDimacs(asolver);
//		Values.randomFuzz(dimacs, LecteurDimacs.class, InputStream.class, PrintWriter.class);
//	}
	
	
}
